\begin{tabbing}
@$i$: with declarations ds:${\it ds}$da:${\it da}$ $k$(v) sends $f$ s v on link $l$($j$)
\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=if eqof(IdDeq)($j$,$i$)\+
\\[0ex]then \=with declarations \+
\\[0ex]ds:${\it ds}$
\\[0ex]da:${\it da}$
\\[0ex]$k$(v) sends $f$ s v on link $l$
\-\\[0ex]else 
\\[0ex]fi 
\-
\end{tabbing}